:- module(basic_constructs, [directive/1,
			     predefined_type/1,
			     predefined_atom/3,
			     predefined_op/5,
			     decompose_body/2,
			     decompose_body/3,
			     meta_formula/2
			    ]).


%% 1. directives, not type-checked ----------------------------
%
directive(consult(_)).
directive(use_module(_)).
directive(ensure_loaded(_)).
directive(module(_)).
directive(use_module(_,_)).
directive(module(_,_)).
directive(op(_,_,_)).
directive(dynamic(_)).
directive(multifile(_)).
directive(load(_)).
directive(load(_,_)).


% 2. predefined types ------------------------------------------------

predefined_type(number).

%

% 3. predefined operators ----------------------------------

predefined_op(+(X,Y),+,[X,Y],[number,number],number).
predefined_op(-(X,Y),-,[X,Y],[number,number],number).
predefined_op(*(X,Y),*,[X,Y],[number,number],number).
predefined_op(//(X,Y),//,[X,Y],[number,number],number).
predefined_op(mod(X,Y),mod,[X,Y],[number,number],number).
predefined_op(+(X),+,[X],[number],number).
predefined_op(-(X),+,[X],[number],number).
predefined_op(abs(X),abs,[X],[number],number).
predefined_op(/(X,Y),/,[X,Y],[number,number],number).
predefined_op(sqrt(X),sqrt,[X],[number], number).
predefined_op(max(X,Y),max,[X,Y],[number,number], number).
predefined_op(**(X,Y),**,[X,Y],[number,number], number).
predefined_op(N,N,[],[], number) :-
	number(N).


% 4. predfined atoms ----------------------------------------------
predefined_atom(true, [], []).
predefined_atom(fail, [], []).
predefined_atom(nl, [], []).
predefined_atom(!, [], []).
predefined_atom(var(X), [X], [_T]).
predefined_atom(X is Y, [X,Y],[number,number]).
predefined_atom(is_in(T,Type), [T], [Type]).
predefined_atom(X=Y, [X,Y], [T,T]).
predefined_atom(X\=Y, [X,Y], [T,T]).
predefined_atom(X<Y, [X,Y], [number,number]).
predefined_atom(X>Y, [X,Y], [number,number]).
predefined_atom(X =<Y, [X,Y], [number,number]).
predefined_atom(X >=Y, [X,Y], [number,number]).
predefined_atom(X =\=Y, [X,Y], [number,number]).
predefined_atom(X =:=Y, [X,Y], [number,number]).
predefined_atom(integer(X), [X], [number]).
predefined_atom(float(X), [X], [number]).

% 6. metaformulas, see below


% body syntax: decomposes a composed formula or a metaformula into a
% list of subformulas (the subformulas of a formula or the
% "involved formulas" in the case of a metaformula)
% ------------------------------------------------------------------

decompose_body(B,D) :-
	decompose_body(B,D,_).

decompose_body(not(A),[A], not) :- !.
decompose_body((A,B),[A,B], and) :- !.
decompose_body((A;B),[A,B], or) :- !.
decompose_body((A->B),[A,B], ->) :- !.
decompose_body((A*->B),[A,B], *->) :- !.
decompose_body(M,[LM], meta) :-
	meta_formula(M,LM), !.


%  meta_formula(M, List):  to type check the metaformula M
%  we have to typecheck the formulas in the list List
%  --------------------------------------------------------------

meta_formula(assert(F),F) :- !.
meta_formula(asserta(F),F) :- !.
meta_formula(assertz(F),F) :- !.
meta_formula(retract(F),F) :- !.
meta_formula(retractall(F),F) :- !.
meta_formula(once(F),F) :- !.
meta_formula(write(_),true) :- !.   %io is not type checked
meta_formula(write(_,_),true) :- !.
meta_formula(writeln(_),true) :- !.
meta_formula(read(_),true) :- !.
meta_formula(read(_,_),true) :- !.
meta_formula(readln(_),true) :- !.
meta_formula(tell(_),true) :- !.
meta_formula(told,true) :- !.
meta_formula(see(_),true) :- !.
meta_formula(seen,true) :- !.
meta_formula(open(_,_,_),true) :- !.
meta_formula(open(_,_,_,_),true) :- !.
meta_formula(close(_),true) :- !.
meta_formula(close(_,_),true) :- !.
meta_formula(throw(_E),true) :- !.  %exceptions are not type cheched
meta_formula(setof(Var,Formula,List), ([Var|List]=[Var|List], Formula)):- !.
meta_formula(bagof(Var,Formula,List), ([Var|List]=[Var|List], Formula)):- !.
meta_formula(forall(Gen,Formula), (Gen, Formula)):- !.
meta_formula(foreach(Gen,Formula), (Gen, Formula)):- !.
meta_formula(Meta,CheckF) :-
	meta_op(Meta,MOp, Called, MArgs),
	(is_var(Called) ->
	      CheckF = ignore(Meta)
	      ;
	      to_call_check(MOp, Called, MArgs, CheckF)
	).

meta_op(Meta, catch ,Called, Args) :-
	Meta =.. [catch, Called | Args], !.
meta_op(Meta, call, Called ,Args) :-
	Meta =.. [call, Called | Args], !.
meta_op(Meta, maplist, Called ,Args) :-
	Meta =.. [maplist, Called | Args].


%  catch(Called,_,_) --> check Called
to_call_check(catch,Called, _, Called) :- !.

%  call(P(AP),Args) --> check P(append(AP,Args))
to_call_check(call,Called, Args, CheckF) :- !,
	Called =.. [P|AP],
	append(AP,Args,AF),
	CheckF =.. [P|AF].

%  maplist(P(AP), L1, .., Lk) -->
%      check (P(AP,X1,..,Xk), L1=[X1|_], .., Lk=[Xk|_])
to_call_check(maplist, Called, Lists, CheckFormula) :- !,
	   Called =..[Pred|AP],
           mkeq(Lists,Vars,Eqns),
	   append(AP,Vars,PArgs),
	   PA =.. [Pred|PArgs],
	   CheckFormula=(PA,Eqns).

is_var(F) :-
	var(F),!;F=variable(_).

mkeq([],[],true).
mkeq([L],[X],L=[X|_]) :- !.
mkeq([L|LS],[X|XS],(L=[X|_],Eqns)) :-
	mkeq(LS,XS,Eqns).

test(MF, CH) :-
     meta_op(MF,MS,F,A,B),
     to_call_list(MS,F,A,B,CH).













